\documentclass[a4paper,10pt,oneside,reqno]{article}

\usepackage{amsfonts, amsmath, amsthm, amssymb}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage[all,cmtip]{xy}
\usepackage{textcomp}
\usepackage{subfloat}
\usepackage{graphicx}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage[utf8]{inputenc}
\usepackage{booktabs}
\usepackage{a4wide}
\usepackage{comment}
\usepackage{array}
\usepackage[colorlinks=true,linkcolor=blue,urlcolor=blue]{hyperref}
\usepackage[lofdepth,lotdepth]{subfig}
\usepackage{tikz}
\usetikzlibrary{decorations.pathreplacing,patterns}
\pagestyle{plain}

\usepackage{array}

%\hypersetup{
%    pdfborder = {0 0 0}
%}

\DeclareMathOperator{\tr}{tr}

\newcommand{\mint}[1]{\text{#1}}
\newcommand{\then}{\Rightarrow}
\newcommand{\Then}{\Longrightarrow}
\newcommand{\trans}{\rightsquigarrow}
\newcommand{\tend}{t_{\text{end}}}

\newcommand{\RushHour}{\textsc{Rush Hour} }
\newcommand{\bddsolve}{\textsc{Bddsolve} }
\newcommand{\game}[1]{\emph{#1}}

\newtheorem*{quest}{Task}
\newtheorem{thm}{Theorem}
\newtheorem{lemma}{Lemma}

%\renewcommand{\thesubsection}{\thesection.\alph{subsection}}

%\frenchspacing

\hypersetup{pdftitle={Rush Hour; Tejiscak}}
\title{Rush Hour}
\author{Matúš Tejiščák (\url{ziman@functor.sk})\\ 4176200}
\date{\today}
\begin{document}

\maketitle

\section{Introduction}

In this paper, we study the possibility to solve the game \RushHour  using
SAT/SMT solvers. We try to design an appropriate encoding of the game and its rules
usable with solvers and experiment with what values of game parameters (board size,
number of blocks) admit a feasible solution.

\subsection{Rush Hour}

\RushHour is a game\footnote{\url{http://en.wikipedia.org/wiki/Rush_Hour_(board_game)}}
by Nob Yoshigahara, similar to the \game{15-puzzle} (also known as \game{Loyd's fifteen}).
On a $6\!\times\! 6$-sized board, different rectangular ($1\!\times\! 2$ or $1\!\times\! 3$)
blocks are placed. These blocks can be slid along their longer sides.

The name \RushHour comes from the interpretation of the game: the blocks within the board
represent cars constraining each other in a limited space, which resembles busy road crossings,
busy parking lots or similar traffic settings.

\begin{figure}[htp]
	\centering
	\begin{tikzpicture}[x=6mm,y=6mm]
		\draw[step=1,gray,dotted] (0,0) grid +(6,6);
		\filldraw[draw=none,pattern=fivepointed stars,pattern color=black!25] (4,3) rectangle +(2,1);
		\begin{scope}[ultra thick,fill=white]
			\filldraw[pattern=crosshatch dots] (0,3) rectangle +(2,1);
			\filldraw (3,5) rectangle +(1,-3);
			\filldraw (3,0) rectangle +(2,1);
		\end{scope}
		\draw (2,3.5) -- ++(3.25,0) -- +(-0.15,0.15) +(0,0) -- +(-0.15,-0.15);
	\end{tikzpicture}
	\caption{An example initial position of a \RushHour game.}
	\label{fig:example}
\end{figure}

The objective of the game is to move the \emph{important} block (filled with dots) to the rightmost
position (visualized by 5-pointed stars in Figure \ref{fig:example}). The intuition behind this is
that the player is sitting in the \emph{important} car and he's trying to get out of the traffic jam
using a road to the right. Cars can move only forward and backward; they cannot turn.

For this purpose, the player must slide other blocks (cars) out of the way of the \emph{important}
block. Finding the strategy which blocks to slide, when and where to slide them is hard and it is the
reason why SAT/SMT solvers are suitable for such a task.

\section{Representation}

We represent the board as a $M{\times}N$ matrix of small natural numbers named $s_{ij}$.
In particular,
\begin{equation}
	s_{ij} = \left \{ \begin{array}{ll}
		k & \text{if the square $(i,j)$ is covered by the car number $k$,} \\
		0 & \text{if the square $(i,j)$ is uncovered.}
    \end{array} \right.
\end{equation}

For example, the position from Figure \ref{fig:example} would be encoded as shown in Figure
\ref{fig:example-coded}. There are three cars, the \emph{important} one always having the number $1$,
the other two having numbers $2$ and $3$, respectively. Empty space is denoted by zeroes.

\begin{figure}[htp]
	\begin{equation}
		s_{ij} = \begin{pmatrix}
			0 &0 &0 &0 &0 &0 \\
			0 &0 &0 &2 &0 &0 \\
			1 &1 &0 &2 &0 &0 \\
			0 &0 &0 &2 &0 &0 \\
			0 &0 &0 &0 &0 &0 \\
			0 &0 &0 &3 &3 &0	
		\end{pmatrix}
	\end{equation}
	\caption{The position from Figure \ref{fig:example} expressed in terms of the matrix $s_{ij}$.}
	\label{fig:example-coded}
\end{figure}

In fact, since this is a \emph{reachability} problem, we use \bddsolve for this task, which requires
decomposing $s_{ij}$ into a binary-representation matrix $s'_{ijk}$, where $k$ ranges over
$\{1\ldots W\}$, $W$ being the desired word width in bits.

To avoid notational clutter, we will consider this binary transformation trivial and we will write all
formulas using the matrix $s_{ij}$ -- although, in the end, our \textsc{Haskell} DSL generates the
three-dimensional matrix $s'$ for \bddsolve to process. However, to preserve a little bit of
distinction, we will use the sign $\equiv$ for this ,,transparent binary equality'', for example
$s_{1,1} \equiv 0$.

\section{Constraints}

\subsection{Initial condition}

The initial condition is trivial since the starting position is given. Hence a specification
such as the one in Figure \ref{fig:example-coded} represents the complete initial condition:

\begin{equation}
  \mathsf{initial} = 
		s_{ij} \equiv \begin{pmatrix}
			0 &0 &0 &0 &0 &0 \\
			0 &0 &0 &2 &0 &0 \\
			1 &1 &0 &2 &0 &0 \\
			0 &0 &0 &2 &0 &0 \\
			0 &0 &0 &0 &0 &0 \\
			0 &0 &0 &3 &3 &0	
		\end{pmatrix}
\end{equation}

\subsection{Final condition}

This one is easy as well: we want the car number $1$ to be in the rightmost position (in the original
\RushHour game it is always sized $2\!\times\! 1$ and it always starts in the third row):
\begin{equation}
	\mathsf{final} = (s_{3,N-1} \equiv 1) \wedge (s_{3,N} \equiv 1)
\end{equation}

\subsection{Transition}

This is the hard part. We assume that the length of blocks is bounded by the number $L$. Then, for
each length (and for each position), we generate shifting rules for blocks.

\begin{equation}
	\mathsf{transition} = \bigvee_{2 \leq l \leq L} \mathsf{availableMoves}(l)
\end{equation}

Now, for every block length, we have four directions the block can move. The predicate \textsf{move}
is parameterized by five numbers: coordinates of the square that represents the ,,front'' of the
car to be moved, length of the block, and two numbers (deltas) representing the direction where the block is situated now.
\begin{align}
	\mathsf{availableMoves}(l) ={}
		& \bigvee_{\substack{i \in \{2\ldots M-l+1\} \\ j \in \{1\ldots N\}}}
			\mathsf{move}(i,j,l-1,1,0) & \text{(downwards)} \\
		& \vee \bigvee_{\substack{i \in \{l \ldots M-1\} \\ j \in \{1 \ldots N\}}}
			\mathsf{move}(i,j,l-1,-1,0) & \text{(upwards)} \\
		& \vee \bigvee_{\substack{i \in \{1 \ldots M\} \\ j \in \{2 \ldots N-l+1\}}}
			\mathsf{move}(i,j,l-1,0,1) & \text{(rightwards)} \\
		& \vee \bigvee_{\substack{i \in \{1 \ldots M\} \\ j \in \{l \ldots N-1\}}}
			\mathsf{move}(i,j,l-1,0,-1) & \text{(leftwards)}
\end{align}

In Figure \ref{fig:move-args}, we describe how the squares relate to each other (what the meaning of
$(i,j)$ is) and what the deltas mean in that context. The gray rectangles are the blocks moving into
the dashed positions.

\begin{figure}[htp]
	\centering
	\subfloat[$\Delta = (0,-1)$]{
		\begin{tikzpicture}[x=5mm,y=5mm]
			\draw[step=1,gray,dotted] (-1,0) grid +(5,5);
			\draw[dashed,ultra thick] (1,2) rectangle +(2,1);
			\filldraw[ultra thick,fill=black!10] (0,2) rectangle +(2,1);
			\draw[thick] (0.5,2.5) -- ++(1,0) -- +(-0.15,0.15) +(0,0) -- +(-0.15,-0.15);
			\draw[->] (3.1,4.5) node[right=-1mm]{$(i,j)$} -- (1.5,4.5) -- (1.5,3.1);
		\end{tikzpicture}
	}
	\subfloat[$\Delta = (0,1)$]{
		\begin{tikzpicture}[x=5mm,y=5mm]
			\draw[step=1,gray,dotted] (-1,0) grid +(5,5);
			\draw[dashed,ultra thick] (0,2) rectangle +(2,1);
			\filldraw[ultra thick,fill=black!10] (1,2) rectangle +(2,1);
			\draw[thick] (2.5,2.5) -- ++(-1,0) -- +(0.15,0.15) +(0,0) -- +(0.15,-0.15);
			\draw[->] (3.1,4.5) node[right=-1mm]{$(i,j)$} -- (1.5,4.5) -- (1.5,3.1);
		\end{tikzpicture}
	}
	\subfloat[$\Delta = (-1,0)$]{
		\begin{tikzpicture}[x=5mm,y=5mm]
			\draw[step=1,gray,dotted] (-1,0) grid +(5,5);
			\draw[dashed,ultra thick] (1,1) rectangle +(1,2);
			\filldraw[ultra thick,fill=black!10] (1,2) rectangle +(1,2);
			\draw[thick] (1.5,3.5) -- ++(0,-1) -- +(0.15,0.15) +(0,0) -- +(-0.15,0.15);
			\draw[->] (3.1,4.1) node[above=-1mm]{$(i,j)$} -- (3.1,2.5) -- (2.1,2.5);
		\end{tikzpicture}
	}
	\subfloat[$\Delta = (1,0)$]{
		\begin{tikzpicture}[x=5mm,y=5mm]
			\draw[step=1,gray,dotted] (-1,0) grid +(5,5);
			\draw[dashed,ultra thick] (1,2) rectangle +(1,2);
			\filldraw[ultra thick,fill=black!10] (1,1) rectangle +(1,2);
			\draw[thick] (1.5,2.5) -- ++(0,1) -- +(0.15,-0.15) +(0,0) -- +(-0.15,-0.15);
			\draw[->] (3.1,4.1) node[above=-1mm]{$(i,j)$} -- (3.1,2.5) -- (2.1,2.5);
		\end{tikzpicture}
	}
	\caption{Illustration of the arguments of the predicate \textsf{move}. Note that the block
	moves \emph{opposite} to $\Delta$.}
	\label{fig:move-args}
\end{figure}

The predicate \textsf{move} is then quite general and captures the notion of moving a puzzle
piece with the given length, at the given position, in the given direction.
\vspace{-3mm}
\begin{align}
	\intertext{$\mathsf{move}(i,j,l,\Delta_i,\Delta_j) ={}$}
	~	&s^0_{ij} \not\equiv 0
			& \text{($(i,j)$ is covered)} \\
		&\wedge \bigvee_{1 \leq k \leq l} s^0_{ij} \equiv s^0_{i+k\Delta_i,j+k\Delta_j}
			& \text{(the block is there)} \\
		&\wedge s^0_{i-\Delta_i,j-\Delta_j} \equiv 0
			& \text{(free square to move into)} \\
		\label{eq:not-longer}
		&\wedge \left\{ \begin{array}{ll}
			\mathsf{true}
				&\text{if $\mathsf{out}\begin{pmatrix}
					i+(l+1)\Delta_i,\\j+(l+1)\Delta_j
				\end{pmatrix}$} \\
			s^0_{ij} \not\equiv s^0_{i+(l+1)\Delta_i,j+(l+1)\Delta_j} &\text{otherwise}
		\end{array} \right. 
			& \text{(block not longer than $l$)}\\
		&\wedge \bigwedge_{(k,l) \notin \left\{\substack{
			(i-\Delta_i,j-\Delta_j)\\(i+l\Delta_i,j+l\Delta_j)} \right.}
			s^1_{kl} \equiv s^0_{kl} 
			& \text{(copy all squares except two)} \\
		&\wedge s^1_{i-\Delta_i,j-\Delta_j} \equiv s^0_{ij}
			& \text{(square covered by the block)} \\
		&\wedge s^1_{i+l\Delta_i,j+l\Delta_j} \equiv 0
			& \text{(square freed by the block)}
\end{align}

It is only in this predicate where we actually manipulate variables. Since we are in a state
transition predicate, we denote $s^0$ the original state and $s^1$ the new state. At the beginning
of the predicate, we check that we can make the move described by $(i,j,l,\Delta_i,\Delta_j)$.
The rest of the predicate describes how the state changes by this transition.

What's left is to define the meta-function\footnote{This function is not represented in the
formula; it is used only as a meta-syntactic shortcut when describing the formula.} \textsf{out},
which has the meaning ,,the square $(i,j)$ is invalid/outside the board''.
\begin{equation}
	\mathsf{out}(i,j) = i < 1 \vee j < 1 \vee i > M \vee j > N
\end{equation}
It is used in Eq. \ref{eq:not-longer}: if a square is out of the board, it definitely does not
belong to the block in question.

\section{Implementation}

We generate the formula for \bddsolve using a \textsc{Haskell} DSL built for this purpose.
The resulting program\footnote{
\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/rush.hs}} is parameterized
by various constants (size of the board, word width in bits, different starting positions).
The formula printed by it is further processed by a \textsc{Perl} script\footnote{
\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/rush-mogrify.pl}} to reorder
variables.

Output of \bddsolve is processed by another \textsc{Perl} script\footnote{
\url{http://code.google.com/p/reasoning-homework/source/browse/trunk/rush-vis.pl}} that adds
pictorial representation to bit vectors printed by \bddsolve.

\section{Solution}

With this implementation, the problem appears to be tractable up to board sizes of
$5\!\times\! 4$, with 3 bits per square (up to 7 blocks), which amounts to 60 Boolean variables.
If we raise any parameter, \bddsolve does not give even a hint of terminating. However,
even $5\!\times\! 4$ allows for some interesting puzzles.

\subsection{Example run}

For an example run, we chose the starting position depicted in Figure \ref{fig:starting-position}.

\begin{figure}[htp]
	\centering
	\begin{tikzpicture}[x=6mm,y=6mm]
		\fill[pattern=fivepointed stars,pattern color=black!25] (3,1) rectangle +(2,1);
		\draw[step=1,gray,dotted] (0,0) grid +(5,4);
		\begin{scope}[ultra thick,fill=white]
			\filldraw[pattern=crosshatch dots] (0,1) rectangle +(2,1);
			\filldraw (0,2) rectangle +(1,2);
			\filldraw (3,0) rectangle +(1,2);
			\filldraw (2,2) rectangle +(3,1);
			\filldraw (2,3) rectangle +(3,1);
		\end{scope}
	\end{tikzpicture}
	\caption{The example starting position.}
	\label{fig:starting-position}
\end{figure}

\bddsolve finds a solution within a fraction of a second. The resulting sequence of moves
contains 11 steps and ends with a correctly solved puzzle. The corresponding consultation can
be seen at the end of the paper, in Section \ref{sec:consultation}.

\section{Discussion and remarks}

There are some silent assumptions and limitations of the program that would be nice to lift, namely:
\begin{itemize}
	\item Length of blocks is either 2 or 3, not more. This is also the case in the original 
		\RushHour puzzle so we keep with this convention here as well.
	\item Board up to $5 \!\times\! 4$, up to 7 blocks. It is interesting that with this setup,
		any starting position was solved instantly. However, if we increment \emph{any} parameter
		(board width, height, bits per square), even with the most trivial starting positions,
		\bddsolve does not terminate. What is it so significant that happens after incrementing
		the parameters? Why does \bddsolve find the solution immediately otherwise?
\end{itemize}

\section{Example consultation}
\label{sec:consultation}

\begin{verbatim}
ziman@idefix:~/dev/reasoning $ sh rush.sh 
bddsolve parameters:
  formula file:       rush.bdd
  bdd node number:    1000000
  bdd cache size:     10000
  stop at solution:   yes

Garbage collection #1: 1000003 nodes / 677285 free / 0.0s / 0.0s total
Garbage collection #2: 1000003 nodes / 294873 free / 0.1s / 0.1s total
  variables:
s_1_1_1_v s_1_1_2_v s_1_1_3_v s_1_2_1_v s_1_2_2_v s_1_2_3_v s_1_3_1_v s_1_3_2_v s_1_3_3_v
s_1_4_1_v s_1_4_2_v s_1_4_3_v s_1_5_1_v s_1_5_2_v s_1_5_3_v s_2_1_1_v s_2_1_2_v s_2_1_3_v
s_2_2_1_v s_2_2_2_v s_2_2_3_v s_2_3_1_v s_2_3_2_v s_2_3_3_v s_2_4_1_v s_2_4_2_v s_2_4_3_v
s_2_5_1_v s_2_5_2_v s_2_5_3_v s_3_1_1_v s_3_1_2_v s_3_1_3_v s_3_2_1_v s_3_2_2_v s_3_2_3_v
s_3_3_1_v s_3_3_2_v s_3_3_3_v s_3_4_1_v s_3_4_2_v s_3_4_3_v s_3_5_1_v s_3_5_2_v s_3_5_3_v
s_4_1_1_v s_4_1_2_v s_4_1_3_v s_4_2_1_v s_4_2_2_v s_4_2_3_v s_4_3_1_v s_4_3_2_v s_4_3_3_v
s_4_4_1_v s_4_4_2_v s_4_4_3_v s_4_5_1_v s_4_5_2_v s_4_5_3_v

------------------------------------------------
-              reach algorithm                 -
------------------------------------------------
iteration     bdd size     # reachable states
    0              60                 1
    1             101                 4
    2             133                 8
    3             172                12
    4             198                16
    5             205                20
    6             242                23
    7             240                25
    8             226                26
    9             256                27
   10             262                28
   11             268                29
   
------------------------------------------------
-              validation                      -
------------------------------------------------
iteration
    0        101000001001001101000110110110100100000010000000000000010000
# . X X X 
# . @ @ @ 
o o . * . 
. . . * . 

    1        101000001001001101000110110110000100100010000000000000010000
# . X X X 
# . @ @ @ 
. o o * . 
. . . * . 

    2        000000001001001101000110110110101100100010000000000000010000
. . X X X 
# . @ @ @ 
# o o * . 
. . . * . 

    3        000000001001001000000110110110101100100010000101000000010000
. . X X X 
. . @ @ @ 
# o o * . 
# . . * . 

    4        000000001001001000110110110000101100100010000101000000010000
. . X X X 
. @ @ @ . 
# o o * . 
# . . * . 

    5        000000001001001110110110000000101100100010000101000000010000
. . X X X 
@ @ @ . . 
# o o * . 
# . . * . 

    6        000000001001001110110110010000101100100010000101000000000000
. . X X X 
@ @ @ * . 
# o o * . 
# . . . . 

    7        000001001001000110110110010000101100100010000101000000000000
. X X X . 
@ @ @ * . 
# o o * . 
# . . . . 

    8        001001001000000110110110010000101100100010000101000000000000
X X X . . 
@ @ @ * . 
# o o * . 
# . . . . 

    9        001001001010000110110110010000101100100000000101000000000000
X X X * . 
@ @ @ * . 
# o o . . 
# . . . . 

   10        001001001010000110110110010000101000100100000101000000000000
X X X * . 
@ @ @ * . 
# . o o . 
# . . . . 

   11        001001001010000110110110010000101000000100100101000000000000
X X X * . 
@ @ @ * . 
# . . o o 
# . . . . 


number of possible transitions   : 691584017778081792
number of reachable final states : 1
0.01 seconds elapsed for solving reach problem
0.01 seconds elapsed for backtracking solution

REACH SUCCEEDED
\end{verbatim}

\end{document}





















































